Nuprl Lemma : quot_elim 13,42

T:Type, E:(TT).
EquivRel(T;x,y.E(x,y))  (ab:T. (a = b  (x,y:T//E(x,y)))  (E(a,b))) 
latex


Upquot 1, quot 1
Definitionsx,yt(x;y), t  T, P  Q, P & Q, P  Q, x(s1,s2), P  Q, , x:AB(x), True, T, S  T
Lemmasequiv rel wf, squash wf, quotient qinc, quotient wf

origin